Left Termination of the query pattern shapes_in_2(g, a) w.r.t. the given Prolog program could successfully be proven:



↳ Prolog
  ↳ PrologToPiTRSProof

Clauses:

shapes(Matrix, N) :- ','(varmat(Matrix, MatrixWithVars), unif_matrx(MatrixWithVars)).
varmat([], []).
varmat(.(L, Ls), .(VL, VLs)) :- ','(varmat(L, VL), varmat(Ls, VLs)).
varmat(.(black, Xs), .(black, VXs)) :- varmat(Xs, VXs).
varmat(.(white, Xs), .(w(X), VXs)) :- varmat(Xs, VXs).
unif_matrx(.(L1, .(L2, Ls))) :- ','(unif_lines(L1, L2), unif_matrx(.(L2, Ls))).
unif_matrx(.(X, [])).
unif_lines(.(W, .(X, L1s)), .(Y, .(Z, L2s))) :- ','(unif_pairs(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))), unif_lines(.(X, L1s), .(Z, L2s))).
unif_lines(.(X, []), .(X1, [])).
unif_pairs([]).
unif_pairs(.(A, .(B, Pairs))) :- ','(unif(A, B), unif_pairs(Pairs)).
unif(w(A), w(A)).
unif(black, black).
unif(black, w(X)).
unif(w(X), black).

Queries:

shapes(g,a).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
shapes_in: (b,f)
varmat_in: (b,f)
unif_matrx_in: (b)
unif_lines_in: (b,b)
unif_pairs_in: (b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_g(MatrixWithVars))
unif_matrx_in_g(.(L1, .(L2, Ls))) → U7_g(L1, L2, Ls, unif_lines_in_gg(L1, L2))
unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_g([]) → unif_pairs_out_g([])
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(A, B, Pairs, unif_in_gg(A, B))
unif_in_gg(w(A), w(A)) → unif_out_gg(w(A), w(A))
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w(X)) → unif_out_gg(black, w(X))
unif_in_gg(w(X), black) → unif_out_gg(w(X), black)
U11_g(A, B, Pairs, unif_out_gg(A, B)) → U12_g(A, B, Pairs, unif_pairs_in_g(Pairs))
U12_g(A, B, Pairs, unif_pairs_out_g(Pairs)) → unif_pairs_out_g(.(A, .(B, Pairs)))
U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg(.(X, []), .(X1, []))
U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_out_gg(.(X, L1s), .(Z, L2s))) → unif_lines_out_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_g(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → U8_g(L1, L2, Ls, unif_matrx_in_g(.(L2, Ls)))
unif_matrx_in_g(.(X, [])) → unif_matrx_out_g(.(X, []))
U8_g(L1, L2, Ls, unif_matrx_out_g(.(L2, Ls))) → unif_matrx_out_g(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_g(MatrixWithVars)) → shapes_out_ga(Matrix, N)

The argument filtering Pi contains the following mapping:
shapes_in_ga(x1, x2)  =  shapes_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
varmat_in_ga(x1, x2)  =  varmat_in_ga(x1)
[]  =  []
varmat_out_ga(x1, x2)  =  varmat_out_ga(x2)
.(x1, x2)  =  .(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x2, x5)
black  =  black
U5_ga(x1, x2, x3)  =  U5_ga(x3)
white  =  white
U6_ga(x1, x2, x3, x4)  =  U6_ga(x4)
w(x1)  =  w
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x3, x5)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
unif_matrx_in_g(x1)  =  unif_matrx_in_g(x1)
U7_g(x1, x2, x3, x4)  =  U7_g(x2, x3, x4)
unif_lines_in_gg(x1, x2)  =  unif_lines_in_gg(x1, x2)
U9_gg(x1, x2, x3, x4, x5, x6, x7)  =  U9_gg(x2, x3, x5, x6, x7)
unif_pairs_in_g(x1)  =  unif_pairs_in_g(x1)
unif_pairs_out_g(x1)  =  unif_pairs_out_g
U11_g(x1, x2, x3, x4)  =  U11_g(x3, x4)
unif_in_gg(x1, x2)  =  unif_in_gg(x1, x2)
unif_out_gg(x1, x2)  =  unif_out_gg
U12_g(x1, x2, x3, x4)  =  U12_g(x4)
U10_gg(x1, x2, x3, x4, x5, x6, x7)  =  U10_gg(x7)
unif_lines_out_gg(x1, x2)  =  unif_lines_out_gg
U8_g(x1, x2, x3, x4)  =  U8_g(x4)
unif_matrx_out_g(x1)  =  unif_matrx_out_g
shapes_out_ga(x1, x2)  =  shapes_out_ga

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_g(MatrixWithVars))
unif_matrx_in_g(.(L1, .(L2, Ls))) → U7_g(L1, L2, Ls, unif_lines_in_gg(L1, L2))
unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_g([]) → unif_pairs_out_g([])
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(A, B, Pairs, unif_in_gg(A, B))
unif_in_gg(w(A), w(A)) → unif_out_gg(w(A), w(A))
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w(X)) → unif_out_gg(black, w(X))
unif_in_gg(w(X), black) → unif_out_gg(w(X), black)
U11_g(A, B, Pairs, unif_out_gg(A, B)) → U12_g(A, B, Pairs, unif_pairs_in_g(Pairs))
U12_g(A, B, Pairs, unif_pairs_out_g(Pairs)) → unif_pairs_out_g(.(A, .(B, Pairs)))
U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg(.(X, []), .(X1, []))
U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_out_gg(.(X, L1s), .(Z, L2s))) → unif_lines_out_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_g(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → U8_g(L1, L2, Ls, unif_matrx_in_g(.(L2, Ls)))
unif_matrx_in_g(.(X, [])) → unif_matrx_out_g(.(X, []))
U8_g(L1, L2, Ls, unif_matrx_out_g(.(L2, Ls))) → unif_matrx_out_g(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_g(MatrixWithVars)) → shapes_out_ga(Matrix, N)

The argument filtering Pi contains the following mapping:
shapes_in_ga(x1, x2)  =  shapes_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
varmat_in_ga(x1, x2)  =  varmat_in_ga(x1)
[]  =  []
varmat_out_ga(x1, x2)  =  varmat_out_ga(x2)
.(x1, x2)  =  .(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x2, x5)
black  =  black
U5_ga(x1, x2, x3)  =  U5_ga(x3)
white  =  white
U6_ga(x1, x2, x3, x4)  =  U6_ga(x4)
w(x1)  =  w
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x3, x5)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
unif_matrx_in_g(x1)  =  unif_matrx_in_g(x1)
U7_g(x1, x2, x3, x4)  =  U7_g(x2, x3, x4)
unif_lines_in_gg(x1, x2)  =  unif_lines_in_gg(x1, x2)
U9_gg(x1, x2, x3, x4, x5, x6, x7)  =  U9_gg(x2, x3, x5, x6, x7)
unif_pairs_in_g(x1)  =  unif_pairs_in_g(x1)
unif_pairs_out_g(x1)  =  unif_pairs_out_g
U11_g(x1, x2, x3, x4)  =  U11_g(x3, x4)
unif_in_gg(x1, x2)  =  unif_in_gg(x1, x2)
unif_out_gg(x1, x2)  =  unif_out_gg
U12_g(x1, x2, x3, x4)  =  U12_g(x4)
U10_gg(x1, x2, x3, x4, x5, x6, x7)  =  U10_gg(x7)
unif_lines_out_gg(x1, x2)  =  unif_lines_out_gg
U8_g(x1, x2, x3, x4)  =  U8_g(x4)
unif_matrx_out_g(x1)  =  unif_matrx_out_g
shapes_out_ga(x1, x2)  =  shapes_out_ga


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

SHAPES_IN_GA(Matrix, N) → U1_GA(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
SHAPES_IN_GA(Matrix, N) → VARMAT_IN_GA(Matrix, MatrixWithVars)
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → U3_GA(L, Ls, VL, VLs, varmat_in_ga(L, VL))
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → VARMAT_IN_GA(L, VL)
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → U5_GA(Xs, VXs, varmat_in_ga(Xs, VXs))
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → VARMAT_IN_GA(Xs, VXs)
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → U6_GA(Xs, X, VXs, varmat_in_ga(Xs, VXs))
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → VARMAT_IN_GA(Xs, VXs)
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_GA(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → VARMAT_IN_GA(Ls, VLs)
U1_GA(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_GA(Matrix, N, unif_matrx_in_g(MatrixWithVars))
U1_GA(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → UNIF_MATRX_IN_G(MatrixWithVars)
UNIF_MATRX_IN_G(.(L1, .(L2, Ls))) → U7_G(L1, L2, Ls, unif_lines_in_gg(L1, L2))
UNIF_MATRX_IN_G(.(L1, .(L2, Ls))) → UNIF_LINES_IN_GG(L1, L2)
UNIF_LINES_IN_GG(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_GG(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
UNIF_LINES_IN_GG(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → UNIF_PAIRS_IN_G(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))
UNIF_PAIRS_IN_G(.(A, .(B, Pairs))) → U11_G(A, B, Pairs, unif_in_gg(A, B))
UNIF_PAIRS_IN_G(.(A, .(B, Pairs))) → UNIF_IN_GG(A, B)
U11_G(A, B, Pairs, unif_out_gg(A, B)) → U12_G(A, B, Pairs, unif_pairs_in_g(Pairs))
U11_G(A, B, Pairs, unif_out_gg(A, B)) → UNIF_PAIRS_IN_G(Pairs)
U9_GG(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_GG(W, X, L1s, Y, Z, L2s, unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
U9_GG(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → UNIF_LINES_IN_GG(.(X, L1s), .(Z, L2s))
U7_G(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → U8_G(L1, L2, Ls, unif_matrx_in_g(.(L2, Ls)))
U7_G(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → UNIF_MATRX_IN_G(.(L2, Ls))

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_g(MatrixWithVars))
unif_matrx_in_g(.(L1, .(L2, Ls))) → U7_g(L1, L2, Ls, unif_lines_in_gg(L1, L2))
unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_g([]) → unif_pairs_out_g([])
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(A, B, Pairs, unif_in_gg(A, B))
unif_in_gg(w(A), w(A)) → unif_out_gg(w(A), w(A))
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w(X)) → unif_out_gg(black, w(X))
unif_in_gg(w(X), black) → unif_out_gg(w(X), black)
U11_g(A, B, Pairs, unif_out_gg(A, B)) → U12_g(A, B, Pairs, unif_pairs_in_g(Pairs))
U12_g(A, B, Pairs, unif_pairs_out_g(Pairs)) → unif_pairs_out_g(.(A, .(B, Pairs)))
U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg(.(X, []), .(X1, []))
U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_out_gg(.(X, L1s), .(Z, L2s))) → unif_lines_out_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_g(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → U8_g(L1, L2, Ls, unif_matrx_in_g(.(L2, Ls)))
unif_matrx_in_g(.(X, [])) → unif_matrx_out_g(.(X, []))
U8_g(L1, L2, Ls, unif_matrx_out_g(.(L2, Ls))) → unif_matrx_out_g(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_g(MatrixWithVars)) → shapes_out_ga(Matrix, N)

The argument filtering Pi contains the following mapping:
shapes_in_ga(x1, x2)  =  shapes_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
varmat_in_ga(x1, x2)  =  varmat_in_ga(x1)
[]  =  []
varmat_out_ga(x1, x2)  =  varmat_out_ga(x2)
.(x1, x2)  =  .(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x2, x5)
black  =  black
U5_ga(x1, x2, x3)  =  U5_ga(x3)
white  =  white
U6_ga(x1, x2, x3, x4)  =  U6_ga(x4)
w(x1)  =  w
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x3, x5)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
unif_matrx_in_g(x1)  =  unif_matrx_in_g(x1)
U7_g(x1, x2, x3, x4)  =  U7_g(x2, x3, x4)
unif_lines_in_gg(x1, x2)  =  unif_lines_in_gg(x1, x2)
U9_gg(x1, x2, x3, x4, x5, x6, x7)  =  U9_gg(x2, x3, x5, x6, x7)
unif_pairs_in_g(x1)  =  unif_pairs_in_g(x1)
unif_pairs_out_g(x1)  =  unif_pairs_out_g
U11_g(x1, x2, x3, x4)  =  U11_g(x3, x4)
unif_in_gg(x1, x2)  =  unif_in_gg(x1, x2)
unif_out_gg(x1, x2)  =  unif_out_gg
U12_g(x1, x2, x3, x4)  =  U12_g(x4)
U10_gg(x1, x2, x3, x4, x5, x6, x7)  =  U10_gg(x7)
unif_lines_out_gg(x1, x2)  =  unif_lines_out_gg
U8_g(x1, x2, x3, x4)  =  U8_g(x4)
unif_matrx_out_g(x1)  =  unif_matrx_out_g
shapes_out_ga(x1, x2)  =  shapes_out_ga
U6_GA(x1, x2, x3, x4)  =  U6_GA(x4)
U7_G(x1, x2, x3, x4)  =  U7_G(x2, x3, x4)
SHAPES_IN_GA(x1, x2)  =  SHAPES_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x3)
U12_G(x1, x2, x3, x4)  =  U12_G(x4)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x3, x5)
U10_GG(x1, x2, x3, x4, x5, x6, x7)  =  U10_GG(x7)
UNIF_IN_GG(x1, x2)  =  UNIF_IN_GG(x1, x2)
U9_GG(x1, x2, x3, x4, x5, x6, x7)  =  U9_GG(x2, x3, x5, x6, x7)
UNIF_PAIRS_IN_G(x1)  =  UNIF_PAIRS_IN_G(x1)
VARMAT_IN_GA(x1, x2)  =  VARMAT_IN_GA(x1)
U8_G(x1, x2, x3, x4)  =  U8_G(x4)
U11_G(x1, x2, x3, x4)  =  U11_G(x3, x4)
UNIF_LINES_IN_GG(x1, x2)  =  UNIF_LINES_IN_GG(x1, x2)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x2, x5)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
UNIF_MATRX_IN_G(x1)  =  UNIF_MATRX_IN_G(x1)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

SHAPES_IN_GA(Matrix, N) → U1_GA(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
SHAPES_IN_GA(Matrix, N) → VARMAT_IN_GA(Matrix, MatrixWithVars)
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → U3_GA(L, Ls, VL, VLs, varmat_in_ga(L, VL))
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → VARMAT_IN_GA(L, VL)
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → U5_GA(Xs, VXs, varmat_in_ga(Xs, VXs))
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → VARMAT_IN_GA(Xs, VXs)
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → U6_GA(Xs, X, VXs, varmat_in_ga(Xs, VXs))
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → VARMAT_IN_GA(Xs, VXs)
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_GA(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → VARMAT_IN_GA(Ls, VLs)
U1_GA(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_GA(Matrix, N, unif_matrx_in_g(MatrixWithVars))
U1_GA(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → UNIF_MATRX_IN_G(MatrixWithVars)
UNIF_MATRX_IN_G(.(L1, .(L2, Ls))) → U7_G(L1, L2, Ls, unif_lines_in_gg(L1, L2))
UNIF_MATRX_IN_G(.(L1, .(L2, Ls))) → UNIF_LINES_IN_GG(L1, L2)
UNIF_LINES_IN_GG(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_GG(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
UNIF_LINES_IN_GG(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → UNIF_PAIRS_IN_G(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))
UNIF_PAIRS_IN_G(.(A, .(B, Pairs))) → U11_G(A, B, Pairs, unif_in_gg(A, B))
UNIF_PAIRS_IN_G(.(A, .(B, Pairs))) → UNIF_IN_GG(A, B)
U11_G(A, B, Pairs, unif_out_gg(A, B)) → U12_G(A, B, Pairs, unif_pairs_in_g(Pairs))
U11_G(A, B, Pairs, unif_out_gg(A, B)) → UNIF_PAIRS_IN_G(Pairs)
U9_GG(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_GG(W, X, L1s, Y, Z, L2s, unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
U9_GG(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → UNIF_LINES_IN_GG(.(X, L1s), .(Z, L2s))
U7_G(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → U8_G(L1, L2, Ls, unif_matrx_in_g(.(L2, Ls)))
U7_G(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → UNIF_MATRX_IN_G(.(L2, Ls))

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_g(MatrixWithVars))
unif_matrx_in_g(.(L1, .(L2, Ls))) → U7_g(L1, L2, Ls, unif_lines_in_gg(L1, L2))
unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_g([]) → unif_pairs_out_g([])
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(A, B, Pairs, unif_in_gg(A, B))
unif_in_gg(w(A), w(A)) → unif_out_gg(w(A), w(A))
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w(X)) → unif_out_gg(black, w(X))
unif_in_gg(w(X), black) → unif_out_gg(w(X), black)
U11_g(A, B, Pairs, unif_out_gg(A, B)) → U12_g(A, B, Pairs, unif_pairs_in_g(Pairs))
U12_g(A, B, Pairs, unif_pairs_out_g(Pairs)) → unif_pairs_out_g(.(A, .(B, Pairs)))
U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg(.(X, []), .(X1, []))
U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_out_gg(.(X, L1s), .(Z, L2s))) → unif_lines_out_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_g(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → U8_g(L1, L2, Ls, unif_matrx_in_g(.(L2, Ls)))
unif_matrx_in_g(.(X, [])) → unif_matrx_out_g(.(X, []))
U8_g(L1, L2, Ls, unif_matrx_out_g(.(L2, Ls))) → unif_matrx_out_g(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_g(MatrixWithVars)) → shapes_out_ga(Matrix, N)

The argument filtering Pi contains the following mapping:
shapes_in_ga(x1, x2)  =  shapes_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
varmat_in_ga(x1, x2)  =  varmat_in_ga(x1)
[]  =  []
varmat_out_ga(x1, x2)  =  varmat_out_ga(x2)
.(x1, x2)  =  .(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x2, x5)
black  =  black
U5_ga(x1, x2, x3)  =  U5_ga(x3)
white  =  white
U6_ga(x1, x2, x3, x4)  =  U6_ga(x4)
w(x1)  =  w
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x3, x5)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
unif_matrx_in_g(x1)  =  unif_matrx_in_g(x1)
U7_g(x1, x2, x3, x4)  =  U7_g(x2, x3, x4)
unif_lines_in_gg(x1, x2)  =  unif_lines_in_gg(x1, x2)
U9_gg(x1, x2, x3, x4, x5, x6, x7)  =  U9_gg(x2, x3, x5, x6, x7)
unif_pairs_in_g(x1)  =  unif_pairs_in_g(x1)
unif_pairs_out_g(x1)  =  unif_pairs_out_g
U11_g(x1, x2, x3, x4)  =  U11_g(x3, x4)
unif_in_gg(x1, x2)  =  unif_in_gg(x1, x2)
unif_out_gg(x1, x2)  =  unif_out_gg
U12_g(x1, x2, x3, x4)  =  U12_g(x4)
U10_gg(x1, x2, x3, x4, x5, x6, x7)  =  U10_gg(x7)
unif_lines_out_gg(x1, x2)  =  unif_lines_out_gg
U8_g(x1, x2, x3, x4)  =  U8_g(x4)
unif_matrx_out_g(x1)  =  unif_matrx_out_g
shapes_out_ga(x1, x2)  =  shapes_out_ga
U6_GA(x1, x2, x3, x4)  =  U6_GA(x4)
U7_G(x1, x2, x3, x4)  =  U7_G(x2, x3, x4)
SHAPES_IN_GA(x1, x2)  =  SHAPES_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x3)
U12_G(x1, x2, x3, x4)  =  U12_G(x4)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x3, x5)
U10_GG(x1, x2, x3, x4, x5, x6, x7)  =  U10_GG(x7)
UNIF_IN_GG(x1, x2)  =  UNIF_IN_GG(x1, x2)
U9_GG(x1, x2, x3, x4, x5, x6, x7)  =  U9_GG(x2, x3, x5, x6, x7)
UNIF_PAIRS_IN_G(x1)  =  UNIF_PAIRS_IN_G(x1)
VARMAT_IN_GA(x1, x2)  =  VARMAT_IN_GA(x1)
U8_G(x1, x2, x3, x4)  =  U8_G(x4)
U11_G(x1, x2, x3, x4)  =  U11_G(x3, x4)
UNIF_LINES_IN_GG(x1, x2)  =  UNIF_LINES_IN_GG(x1, x2)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x2, x5)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
UNIF_MATRX_IN_G(x1)  =  UNIF_MATRX_IN_G(x1)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 4 SCCs with 13 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

UNIF_PAIRS_IN_G(.(A, .(B, Pairs))) → U11_G(A, B, Pairs, unif_in_gg(A, B))
U11_G(A, B, Pairs, unif_out_gg(A, B)) → UNIF_PAIRS_IN_G(Pairs)

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_g(MatrixWithVars))
unif_matrx_in_g(.(L1, .(L2, Ls))) → U7_g(L1, L2, Ls, unif_lines_in_gg(L1, L2))
unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_g([]) → unif_pairs_out_g([])
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(A, B, Pairs, unif_in_gg(A, B))
unif_in_gg(w(A), w(A)) → unif_out_gg(w(A), w(A))
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w(X)) → unif_out_gg(black, w(X))
unif_in_gg(w(X), black) → unif_out_gg(w(X), black)
U11_g(A, B, Pairs, unif_out_gg(A, B)) → U12_g(A, B, Pairs, unif_pairs_in_g(Pairs))
U12_g(A, B, Pairs, unif_pairs_out_g(Pairs)) → unif_pairs_out_g(.(A, .(B, Pairs)))
U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg(.(X, []), .(X1, []))
U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_out_gg(.(X, L1s), .(Z, L2s))) → unif_lines_out_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_g(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → U8_g(L1, L2, Ls, unif_matrx_in_g(.(L2, Ls)))
unif_matrx_in_g(.(X, [])) → unif_matrx_out_g(.(X, []))
U8_g(L1, L2, Ls, unif_matrx_out_g(.(L2, Ls))) → unif_matrx_out_g(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_g(MatrixWithVars)) → shapes_out_ga(Matrix, N)

The argument filtering Pi contains the following mapping:
shapes_in_ga(x1, x2)  =  shapes_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
varmat_in_ga(x1, x2)  =  varmat_in_ga(x1)
[]  =  []
varmat_out_ga(x1, x2)  =  varmat_out_ga(x2)
.(x1, x2)  =  .(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x2, x5)
black  =  black
U5_ga(x1, x2, x3)  =  U5_ga(x3)
white  =  white
U6_ga(x1, x2, x3, x4)  =  U6_ga(x4)
w(x1)  =  w
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x3, x5)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
unif_matrx_in_g(x1)  =  unif_matrx_in_g(x1)
U7_g(x1, x2, x3, x4)  =  U7_g(x2, x3, x4)
unif_lines_in_gg(x1, x2)  =  unif_lines_in_gg(x1, x2)
U9_gg(x1, x2, x3, x4, x5, x6, x7)  =  U9_gg(x2, x3, x5, x6, x7)
unif_pairs_in_g(x1)  =  unif_pairs_in_g(x1)
unif_pairs_out_g(x1)  =  unif_pairs_out_g
U11_g(x1, x2, x3, x4)  =  U11_g(x3, x4)
unif_in_gg(x1, x2)  =  unif_in_gg(x1, x2)
unif_out_gg(x1, x2)  =  unif_out_gg
U12_g(x1, x2, x3, x4)  =  U12_g(x4)
U10_gg(x1, x2, x3, x4, x5, x6, x7)  =  U10_gg(x7)
unif_lines_out_gg(x1, x2)  =  unif_lines_out_gg
U8_g(x1, x2, x3, x4)  =  U8_g(x4)
unif_matrx_out_g(x1)  =  unif_matrx_out_g
shapes_out_ga(x1, x2)  =  shapes_out_ga
UNIF_PAIRS_IN_G(x1)  =  UNIF_PAIRS_IN_G(x1)
U11_G(x1, x2, x3, x4)  =  U11_G(x3, x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

UNIF_PAIRS_IN_G(.(A, .(B, Pairs))) → U11_G(A, B, Pairs, unif_in_gg(A, B))
U11_G(A, B, Pairs, unif_out_gg(A, B)) → UNIF_PAIRS_IN_G(Pairs)

The TRS R consists of the following rules:

unif_in_gg(w(A), w(A)) → unif_out_gg(w(A), w(A))
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w(X)) → unif_out_gg(black, w(X))
unif_in_gg(w(X), black) → unif_out_gg(w(X), black)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
black  =  black
w(x1)  =  w
unif_in_gg(x1, x2)  =  unif_in_gg(x1, x2)
unif_out_gg(x1, x2)  =  unif_out_gg
UNIF_PAIRS_IN_G(x1)  =  UNIF_PAIRS_IN_G(x1)
U11_G(x1, x2, x3, x4)  =  U11_G(x3, x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

U11_G(Pairs, unif_out_gg) → UNIF_PAIRS_IN_G(Pairs)
UNIF_PAIRS_IN_G(.(A, .(B, Pairs))) → U11_G(Pairs, unif_in_gg(A, B))

The TRS R consists of the following rules:

unif_in_gg(w, w) → unif_out_gg
unif_in_gg(black, black) → unif_out_gg
unif_in_gg(black, w) → unif_out_gg
unif_in_gg(w, black) → unif_out_gg

The set Q consists of the following terms:

unif_in_gg(x0, x1)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

U9_GG(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → UNIF_LINES_IN_GG(.(X, L1s), .(Z, L2s))
UNIF_LINES_IN_GG(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_GG(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_g(MatrixWithVars))
unif_matrx_in_g(.(L1, .(L2, Ls))) → U7_g(L1, L2, Ls, unif_lines_in_gg(L1, L2))
unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_g([]) → unif_pairs_out_g([])
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(A, B, Pairs, unif_in_gg(A, B))
unif_in_gg(w(A), w(A)) → unif_out_gg(w(A), w(A))
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w(X)) → unif_out_gg(black, w(X))
unif_in_gg(w(X), black) → unif_out_gg(w(X), black)
U11_g(A, B, Pairs, unif_out_gg(A, B)) → U12_g(A, B, Pairs, unif_pairs_in_g(Pairs))
U12_g(A, B, Pairs, unif_pairs_out_g(Pairs)) → unif_pairs_out_g(.(A, .(B, Pairs)))
U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg(.(X, []), .(X1, []))
U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_out_gg(.(X, L1s), .(Z, L2s))) → unif_lines_out_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_g(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → U8_g(L1, L2, Ls, unif_matrx_in_g(.(L2, Ls)))
unif_matrx_in_g(.(X, [])) → unif_matrx_out_g(.(X, []))
U8_g(L1, L2, Ls, unif_matrx_out_g(.(L2, Ls))) → unif_matrx_out_g(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_g(MatrixWithVars)) → shapes_out_ga(Matrix, N)

The argument filtering Pi contains the following mapping:
shapes_in_ga(x1, x2)  =  shapes_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
varmat_in_ga(x1, x2)  =  varmat_in_ga(x1)
[]  =  []
varmat_out_ga(x1, x2)  =  varmat_out_ga(x2)
.(x1, x2)  =  .(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x2, x5)
black  =  black
U5_ga(x1, x2, x3)  =  U5_ga(x3)
white  =  white
U6_ga(x1, x2, x3, x4)  =  U6_ga(x4)
w(x1)  =  w
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x3, x5)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
unif_matrx_in_g(x1)  =  unif_matrx_in_g(x1)
U7_g(x1, x2, x3, x4)  =  U7_g(x2, x3, x4)
unif_lines_in_gg(x1, x2)  =  unif_lines_in_gg(x1, x2)
U9_gg(x1, x2, x3, x4, x5, x6, x7)  =  U9_gg(x2, x3, x5, x6, x7)
unif_pairs_in_g(x1)  =  unif_pairs_in_g(x1)
unif_pairs_out_g(x1)  =  unif_pairs_out_g
U11_g(x1, x2, x3, x4)  =  U11_g(x3, x4)
unif_in_gg(x1, x2)  =  unif_in_gg(x1, x2)
unif_out_gg(x1, x2)  =  unif_out_gg
U12_g(x1, x2, x3, x4)  =  U12_g(x4)
U10_gg(x1, x2, x3, x4, x5, x6, x7)  =  U10_gg(x7)
unif_lines_out_gg(x1, x2)  =  unif_lines_out_gg
U8_g(x1, x2, x3, x4)  =  U8_g(x4)
unif_matrx_out_g(x1)  =  unif_matrx_out_g
shapes_out_ga(x1, x2)  =  shapes_out_ga
U9_GG(x1, x2, x3, x4, x5, x6, x7)  =  U9_GG(x2, x3, x5, x6, x7)
UNIF_LINES_IN_GG(x1, x2)  =  UNIF_LINES_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

U9_GG(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → UNIF_LINES_IN_GG(.(X, L1s), .(Z, L2s))
UNIF_LINES_IN_GG(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_GG(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))

The TRS R consists of the following rules:

unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(A, B, Pairs, unif_in_gg(A, B))
U11_g(A, B, Pairs, unif_out_gg(A, B)) → U12_g(A, B, Pairs, unif_pairs_in_g(Pairs))
unif_in_gg(w(A), w(A)) → unif_out_gg(w(A), w(A))
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w(X)) → unif_out_gg(black, w(X))
unif_in_gg(w(X), black) → unif_out_gg(w(X), black)
U12_g(A, B, Pairs, unif_pairs_out_g(Pairs)) → unif_pairs_out_g(.(A, .(B, Pairs)))
unif_pairs_in_g([]) → unif_pairs_out_g([])

The argument filtering Pi contains the following mapping:
[]  =  []
.(x1, x2)  =  .(x1, x2)
black  =  black
w(x1)  =  w
unif_pairs_in_g(x1)  =  unif_pairs_in_g(x1)
unif_pairs_out_g(x1)  =  unif_pairs_out_g
U11_g(x1, x2, x3, x4)  =  U11_g(x3, x4)
unif_in_gg(x1, x2)  =  unif_in_gg(x1, x2)
unif_out_gg(x1, x2)  =  unif_out_gg
U12_g(x1, x2, x3, x4)  =  U12_g(x4)
U9_GG(x1, x2, x3, x4, x5, x6, x7)  =  U9_GG(x2, x3, x5, x6, x7)
UNIF_LINES_IN_GG(x1, x2)  =  UNIF_LINES_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Rewriting
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

UNIF_LINES_IN_GG(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_GG(X, L1s, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
U9_GG(X, L1s, Z, L2s, unif_pairs_out_g) → UNIF_LINES_IN_GG(.(X, L1s), .(Z, L2s))

The TRS R consists of the following rules:

unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(Pairs, unif_in_gg(A, B))
U11_g(Pairs, unif_out_gg) → U12_g(unif_pairs_in_g(Pairs))
unif_in_gg(w, w) → unif_out_gg
unif_in_gg(black, black) → unif_out_gg
unif_in_gg(black, w) → unif_out_gg
unif_in_gg(w, black) → unif_out_gg
U12_g(unif_pairs_out_g) → unif_pairs_out_g
unif_pairs_in_g([]) → unif_pairs_out_g

The set Q consists of the following terms:

unif_pairs_in_g(x0)
U11_g(x0, x1)
unif_in_gg(x0, x1)
U12_g(x0)

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule UNIF_LINES_IN_GG(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_GG(X, L1s, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) at position [4] we obtained the following new rules:

UNIF_LINES_IN_GG(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_GG(X, L1s, Z, L2s, U11_g(.(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))), unif_in_gg(W, X)))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Rewriting
                          ↳ QDP
                            ↳ QDPOrderProof
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

U9_GG(X, L1s, Z, L2s, unif_pairs_out_g) → UNIF_LINES_IN_GG(.(X, L1s), .(Z, L2s))
UNIF_LINES_IN_GG(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_GG(X, L1s, Z, L2s, U11_g(.(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))), unif_in_gg(W, X)))

The TRS R consists of the following rules:

unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(Pairs, unif_in_gg(A, B))
U11_g(Pairs, unif_out_gg) → U12_g(unif_pairs_in_g(Pairs))
unif_in_gg(w, w) → unif_out_gg
unif_in_gg(black, black) → unif_out_gg
unif_in_gg(black, w) → unif_out_gg
unif_in_gg(w, black) → unif_out_gg
U12_g(unif_pairs_out_g) → unif_pairs_out_g
unif_pairs_in_g([]) → unif_pairs_out_g

The set Q consists of the following terms:

unif_pairs_in_g(x0)
U11_g(x0, x1)
unif_in_gg(x0, x1)
U12_g(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


U9_GG(X, L1s, Z, L2s, unif_pairs_out_g) → UNIF_LINES_IN_GG(.(X, L1s), .(Z, L2s))
UNIF_LINES_IN_GG(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_GG(X, L1s, Z, L2s, U11_g(.(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))), unif_in_gg(W, X)))
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
U9_GG(x1, x2, x3, x4, x5)  =  U9_GG(x4, x5)
unif_pairs_out_g  =  unif_pairs_out_g
UNIF_LINES_IN_GG(x1, x2)  =  UNIF_LINES_IN_GG(x2)
.(x1, x2)  =  .(x2)
U11_g(x1, x2)  =  U11_g(x2)
[]  =  []
unif_in_gg(x1, x2)  =  unif_in_gg
w  =  w
unif_out_gg  =  unif_out_gg
U12_g(x1)  =  U12_g
black  =  black
unif_pairs_in_g(x1)  =  unif_pairs_in_g

Recursive path order with status [2].
Quasi-Precedence:
w > [unifpairsoutg, U11g1, [], unifoutgg, U12g, black]
unifpairsing > [U9GG2, .1, unifingg] > UNIFLINESINGG1 > [unifpairsoutg, U11g1, [], unifoutgg, U12g, black]

Status:
U11g1: [1]
unifpairsing: multiset
UNIFLINESINGG1: [1]
[]: multiset
black: multiset
U12g: []
unifpairsoutg: multiset
unifingg: multiset
.1: multiset
U9GG2: multiset
unifoutgg: multiset
w: multiset


The following usable rules [17] were oriented:

unif_in_gg(w, w) → unif_out_gg
U12_g(unif_pairs_out_g) → unif_pairs_out_g
unif_in_gg(black, w) → unif_out_gg
U11_g(Pairs, unif_out_gg) → U12_g(unif_pairs_in_g(Pairs))
unif_in_gg(black, black) → unif_out_gg
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(Pairs, unif_in_gg(A, B))
unif_in_gg(w, black) → unif_out_gg



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Rewriting
                          ↳ QDP
                            ↳ QDPOrderProof
                              ↳ QDP
                                ↳ PisEmptyProof
              ↳ PiDP
              ↳ PiDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(Pairs, unif_in_gg(A, B))
U11_g(Pairs, unif_out_gg) → U12_g(unif_pairs_in_g(Pairs))
unif_in_gg(w, w) → unif_out_gg
unif_in_gg(black, black) → unif_out_gg
unif_in_gg(black, w) → unif_out_gg
unif_in_gg(w, black) → unif_out_gg
U12_g(unif_pairs_out_g) → unif_pairs_out_g
unif_pairs_in_g([]) → unif_pairs_out_g

The set Q consists of the following terms:

unif_pairs_in_g(x0)
U11_g(x0, x1)
unif_in_gg(x0, x1)
U12_g(x0)

We have to consider all (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

U7_G(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → UNIF_MATRX_IN_G(.(L2, Ls))
UNIF_MATRX_IN_G(.(L1, .(L2, Ls))) → U7_G(L1, L2, Ls, unif_lines_in_gg(L1, L2))

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_g(MatrixWithVars))
unif_matrx_in_g(.(L1, .(L2, Ls))) → U7_g(L1, L2, Ls, unif_lines_in_gg(L1, L2))
unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_g([]) → unif_pairs_out_g([])
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(A, B, Pairs, unif_in_gg(A, B))
unif_in_gg(w(A), w(A)) → unif_out_gg(w(A), w(A))
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w(X)) → unif_out_gg(black, w(X))
unif_in_gg(w(X), black) → unif_out_gg(w(X), black)
U11_g(A, B, Pairs, unif_out_gg(A, B)) → U12_g(A, B, Pairs, unif_pairs_in_g(Pairs))
U12_g(A, B, Pairs, unif_pairs_out_g(Pairs)) → unif_pairs_out_g(.(A, .(B, Pairs)))
U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg(.(X, []), .(X1, []))
U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_out_gg(.(X, L1s), .(Z, L2s))) → unif_lines_out_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_g(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → U8_g(L1, L2, Ls, unif_matrx_in_g(.(L2, Ls)))
unif_matrx_in_g(.(X, [])) → unif_matrx_out_g(.(X, []))
U8_g(L1, L2, Ls, unif_matrx_out_g(.(L2, Ls))) → unif_matrx_out_g(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_g(MatrixWithVars)) → shapes_out_ga(Matrix, N)

The argument filtering Pi contains the following mapping:
shapes_in_ga(x1, x2)  =  shapes_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
varmat_in_ga(x1, x2)  =  varmat_in_ga(x1)
[]  =  []
varmat_out_ga(x1, x2)  =  varmat_out_ga(x2)
.(x1, x2)  =  .(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x2, x5)
black  =  black
U5_ga(x1, x2, x3)  =  U5_ga(x3)
white  =  white
U6_ga(x1, x2, x3, x4)  =  U6_ga(x4)
w(x1)  =  w
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x3, x5)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
unif_matrx_in_g(x1)  =  unif_matrx_in_g(x1)
U7_g(x1, x2, x3, x4)  =  U7_g(x2, x3, x4)
unif_lines_in_gg(x1, x2)  =  unif_lines_in_gg(x1, x2)
U9_gg(x1, x2, x3, x4, x5, x6, x7)  =  U9_gg(x2, x3, x5, x6, x7)
unif_pairs_in_g(x1)  =  unif_pairs_in_g(x1)
unif_pairs_out_g(x1)  =  unif_pairs_out_g
U11_g(x1, x2, x3, x4)  =  U11_g(x3, x4)
unif_in_gg(x1, x2)  =  unif_in_gg(x1, x2)
unif_out_gg(x1, x2)  =  unif_out_gg
U12_g(x1, x2, x3, x4)  =  U12_g(x4)
U10_gg(x1, x2, x3, x4, x5, x6, x7)  =  U10_gg(x7)
unif_lines_out_gg(x1, x2)  =  unif_lines_out_gg
U8_g(x1, x2, x3, x4)  =  U8_g(x4)
unif_matrx_out_g(x1)  =  unif_matrx_out_g
shapes_out_ga(x1, x2)  =  shapes_out_ga
U7_G(x1, x2, x3, x4)  =  U7_G(x2, x3, x4)
UNIF_MATRX_IN_G(x1)  =  UNIF_MATRX_IN_G(x1)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

U7_G(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → UNIF_MATRX_IN_G(.(L2, Ls))
UNIF_MATRX_IN_G(.(L1, .(L2, Ls))) → U7_G(L1, L2, Ls, unif_lines_in_gg(L1, L2))

The TRS R consists of the following rules:

unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg(.(X, []), .(X1, []))
U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(A, B, Pairs, unif_in_gg(A, B))
U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_out_gg(.(X, L1s), .(Z, L2s))) → unif_lines_out_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U11_g(A, B, Pairs, unif_out_gg(A, B)) → U12_g(A, B, Pairs, unif_pairs_in_g(Pairs))
unif_in_gg(w(A), w(A)) → unif_out_gg(w(A), w(A))
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w(X)) → unif_out_gg(black, w(X))
unif_in_gg(w(X), black) → unif_out_gg(w(X), black)
U12_g(A, B, Pairs, unif_pairs_out_g(Pairs)) → unif_pairs_out_g(.(A, .(B, Pairs)))
unif_pairs_in_g([]) → unif_pairs_out_g([])

The argument filtering Pi contains the following mapping:
[]  =  []
.(x1, x2)  =  .(x1, x2)
black  =  black
w(x1)  =  w
unif_lines_in_gg(x1, x2)  =  unif_lines_in_gg(x1, x2)
U9_gg(x1, x2, x3, x4, x5, x6, x7)  =  U9_gg(x2, x3, x5, x6, x7)
unif_pairs_in_g(x1)  =  unif_pairs_in_g(x1)
unif_pairs_out_g(x1)  =  unif_pairs_out_g
U11_g(x1, x2, x3, x4)  =  U11_g(x3, x4)
unif_in_gg(x1, x2)  =  unif_in_gg(x1, x2)
unif_out_gg(x1, x2)  =  unif_out_gg
U12_g(x1, x2, x3, x4)  =  U12_g(x4)
U10_gg(x1, x2, x3, x4, x5, x6, x7)  =  U10_gg(x7)
unif_lines_out_gg(x1, x2)  =  unif_lines_out_gg
U7_G(x1, x2, x3, x4)  =  U7_G(x2, x3, x4)
UNIF_MATRX_IN_G(x1)  =  UNIF_MATRX_IN_G(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPOrderProof
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

U7_G(L2, Ls, unif_lines_out_gg) → UNIF_MATRX_IN_G(.(L2, Ls))
UNIF_MATRX_IN_G(.(L1, .(L2, Ls))) → U7_G(L2, Ls, unif_lines_in_gg(L1, L2))

The TRS R consists of the following rules:

unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(X, L1s, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg
U9_gg(X, L1s, Z, L2s, unif_pairs_out_g) → U10_gg(unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(Pairs, unif_in_gg(A, B))
U10_gg(unif_lines_out_gg) → unif_lines_out_gg
U11_g(Pairs, unif_out_gg) → U12_g(unif_pairs_in_g(Pairs))
unif_in_gg(w, w) → unif_out_gg
unif_in_gg(black, black) → unif_out_gg
unif_in_gg(black, w) → unif_out_gg
unif_in_gg(w, black) → unif_out_gg
U12_g(unif_pairs_out_g) → unif_pairs_out_g
unif_pairs_in_g([]) → unif_pairs_out_g

The set Q consists of the following terms:

unif_lines_in_gg(x0, x1)
U9_gg(x0, x1, x2, x3, x4)
unif_pairs_in_g(x0)
U10_gg(x0)
U11_g(x0, x1)
unif_in_gg(x0, x1)
U12_g(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


UNIF_MATRX_IN_G(.(L1, .(L2, Ls))) → U7_G(L2, Ls, unif_lines_in_gg(L1, L2))
The remaining pairs can at least be oriented weakly.

U7_G(L2, Ls, unif_lines_out_gg) → UNIF_MATRX_IN_G(.(L2, Ls))
Used ordering: Polynomial interpretation [25]:

POL(.(x1, x2)) = 1 + x1 + x2   
POL(U10_gg(x1)) = 1   
POL(U11_g(x1, x2)) = 1 + x2   
POL(U12_g(x1)) = 0   
POL(U7_G(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(U9_gg(x1, x2, x3, x4, x5)) = 1 + x1 + x2   
POL(UNIF_MATRX_IN_G(x1)) = 1 + x1   
POL([]) = 0   
POL(black) = 0   
POL(unif_in_gg(x1, x2)) = 0   
POL(unif_lines_in_gg(x1, x2)) = x1   
POL(unif_lines_out_gg) = 1   
POL(unif_out_gg) = 1   
POL(unif_pairs_in_g(x1)) = 1   
POL(unif_pairs_out_g) = 0   
POL(w) = 0   

The following usable rules [17] were oriented:

unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg
unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(X, L1s, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
U9_gg(X, L1s, Z, L2s, unif_pairs_out_g) → U10_gg(unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
U10_gg(unif_lines_out_gg) → unif_lines_out_gg



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPOrderProof
                          ↳ QDP
                            ↳ DependencyGraphProof
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

U7_G(L2, Ls, unif_lines_out_gg) → UNIF_MATRX_IN_G(.(L2, Ls))

The TRS R consists of the following rules:

unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(X, L1s, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg
U9_gg(X, L1s, Z, L2s, unif_pairs_out_g) → U10_gg(unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(Pairs, unif_in_gg(A, B))
U10_gg(unif_lines_out_gg) → unif_lines_out_gg
U11_g(Pairs, unif_out_gg) → U12_g(unif_pairs_in_g(Pairs))
unif_in_gg(w, w) → unif_out_gg
unif_in_gg(black, black) → unif_out_gg
unif_in_gg(black, w) → unif_out_gg
unif_in_gg(w, black) → unif_out_gg
U12_g(unif_pairs_out_g) → unif_pairs_out_g
unif_pairs_in_g([]) → unif_pairs_out_g

The set Q consists of the following terms:

unif_lines_in_gg(x0, x1)
U9_gg(x0, x1, x2, x3, x4)
unif_pairs_in_g(x0)
U10_gg(x0)
U11_g(x0, x1)
unif_in_gg(x0, x1)
U12_g(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → VARMAT_IN_GA(L, VL)
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → VARMAT_IN_GA(Ls, VLs)
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → U3_GA(L, Ls, VL, VLs, varmat_in_ga(L, VL))
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → VARMAT_IN_GA(Xs, VXs)
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → VARMAT_IN_GA(Xs, VXs)

The TRS R consists of the following rules:

shapes_in_ga(Matrix, N) → U1_ga(Matrix, N, varmat_in_ga(Matrix, MatrixWithVars))
varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))
U1_ga(Matrix, N, varmat_out_ga(Matrix, MatrixWithVars)) → U2_ga(Matrix, N, unif_matrx_in_g(MatrixWithVars))
unif_matrx_in_g(.(L1, .(L2, Ls))) → U7_g(L1, L2, Ls, unif_lines_in_gg(L1, L2))
unif_lines_in_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s))) → U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_in_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, []))))))))))))))
unif_pairs_in_g([]) → unif_pairs_out_g([])
unif_pairs_in_g(.(A, .(B, Pairs))) → U11_g(A, B, Pairs, unif_in_gg(A, B))
unif_in_gg(w(A), w(A)) → unif_out_gg(w(A), w(A))
unif_in_gg(black, black) → unif_out_gg(black, black)
unif_in_gg(black, w(X)) → unif_out_gg(black, w(X))
unif_in_gg(w(X), black) → unif_out_gg(w(X), black)
U11_g(A, B, Pairs, unif_out_gg(A, B)) → U12_g(A, B, Pairs, unif_pairs_in_g(Pairs))
U12_g(A, B, Pairs, unif_pairs_out_g(Pairs)) → unif_pairs_out_g(.(A, .(B, Pairs)))
U9_gg(W, X, L1s, Y, Z, L2s, unif_pairs_out_g(.(W, .(X, .(Y, .(Z, .(W, .(Y, .(X, .(Z, .(W, .(Z, .(X, .(Y, [])))))))))))))) → U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_in_gg(.(X, L1s), .(Z, L2s)))
unif_lines_in_gg(.(X, []), .(X1, [])) → unif_lines_out_gg(.(X, []), .(X1, []))
U10_gg(W, X, L1s, Y, Z, L2s, unif_lines_out_gg(.(X, L1s), .(Z, L2s))) → unif_lines_out_gg(.(W, .(X, L1s)), .(Y, .(Z, L2s)))
U7_g(L1, L2, Ls, unif_lines_out_gg(L1, L2)) → U8_g(L1, L2, Ls, unif_matrx_in_g(.(L2, Ls)))
unif_matrx_in_g(.(X, [])) → unif_matrx_out_g(.(X, []))
U8_g(L1, L2, Ls, unif_matrx_out_g(.(L2, Ls))) → unif_matrx_out_g(.(L1, .(L2, Ls)))
U2_ga(Matrix, N, unif_matrx_out_g(MatrixWithVars)) → shapes_out_ga(Matrix, N)

The argument filtering Pi contains the following mapping:
shapes_in_ga(x1, x2)  =  shapes_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
varmat_in_ga(x1, x2)  =  varmat_in_ga(x1)
[]  =  []
varmat_out_ga(x1, x2)  =  varmat_out_ga(x2)
.(x1, x2)  =  .(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x2, x5)
black  =  black
U5_ga(x1, x2, x3)  =  U5_ga(x3)
white  =  white
U6_ga(x1, x2, x3, x4)  =  U6_ga(x4)
w(x1)  =  w
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x3, x5)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
unif_matrx_in_g(x1)  =  unif_matrx_in_g(x1)
U7_g(x1, x2, x3, x4)  =  U7_g(x2, x3, x4)
unif_lines_in_gg(x1, x2)  =  unif_lines_in_gg(x1, x2)
U9_gg(x1, x2, x3, x4, x5, x6, x7)  =  U9_gg(x2, x3, x5, x6, x7)
unif_pairs_in_g(x1)  =  unif_pairs_in_g(x1)
unif_pairs_out_g(x1)  =  unif_pairs_out_g
U11_g(x1, x2, x3, x4)  =  U11_g(x3, x4)
unif_in_gg(x1, x2)  =  unif_in_gg(x1, x2)
unif_out_gg(x1, x2)  =  unif_out_gg
U12_g(x1, x2, x3, x4)  =  U12_g(x4)
U10_gg(x1, x2, x3, x4, x5, x6, x7)  =  U10_gg(x7)
unif_lines_out_gg(x1, x2)  =  unif_lines_out_gg
U8_g(x1, x2, x3, x4)  =  U8_g(x4)
unif_matrx_out_g(x1)  =  unif_matrx_out_g
shapes_out_ga(x1, x2)  =  shapes_out_ga
VARMAT_IN_GA(x1, x2)  =  VARMAT_IN_GA(x1)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x2, x5)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → VARMAT_IN_GA(L, VL)
U3_GA(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → VARMAT_IN_GA(Ls, VLs)
VARMAT_IN_GA(.(L, Ls), .(VL, VLs)) → U3_GA(L, Ls, VL, VLs, varmat_in_ga(L, VL))
VARMAT_IN_GA(.(black, Xs), .(black, VXs)) → VARMAT_IN_GA(Xs, VXs)
VARMAT_IN_GA(.(white, Xs), .(w(X), VXs)) → VARMAT_IN_GA(Xs, VXs)

The TRS R consists of the following rules:

varmat_in_ga([], []) → varmat_out_ga([], [])
varmat_in_ga(.(L, Ls), .(VL, VLs)) → U3_ga(L, Ls, VL, VLs, varmat_in_ga(L, VL))
varmat_in_ga(.(black, Xs), .(black, VXs)) → U5_ga(Xs, VXs, varmat_in_ga(Xs, VXs))
varmat_in_ga(.(white, Xs), .(w(X), VXs)) → U6_ga(Xs, X, VXs, varmat_in_ga(Xs, VXs))
U3_ga(L, Ls, VL, VLs, varmat_out_ga(L, VL)) → U4_ga(L, Ls, VL, VLs, varmat_in_ga(Ls, VLs))
U5_ga(Xs, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(black, Xs), .(black, VXs))
U6_ga(Xs, X, VXs, varmat_out_ga(Xs, VXs)) → varmat_out_ga(.(white, Xs), .(w(X), VXs))
U4_ga(L, Ls, VL, VLs, varmat_out_ga(Ls, VLs)) → varmat_out_ga(.(L, Ls), .(VL, VLs))

The argument filtering Pi contains the following mapping:
varmat_in_ga(x1, x2)  =  varmat_in_ga(x1)
[]  =  []
varmat_out_ga(x1, x2)  =  varmat_out_ga(x2)
.(x1, x2)  =  .(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x2, x5)
black  =  black
U5_ga(x1, x2, x3)  =  U5_ga(x3)
white  =  white
U6_ga(x1, x2, x3, x4)  =  U6_ga(x4)
w(x1)  =  w
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x3, x5)
VARMAT_IN_GA(x1, x2)  =  VARMAT_IN_GA(x1)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x2, x5)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

VARMAT_IN_GA(.(black, Xs)) → VARMAT_IN_GA(Xs)
VARMAT_IN_GA(.(L, Ls)) → VARMAT_IN_GA(L)
VARMAT_IN_GA(.(L, Ls)) → U3_GA(Ls, varmat_in_ga(L))
U3_GA(Ls, varmat_out_ga(VL)) → VARMAT_IN_GA(Ls)
VARMAT_IN_GA(.(white, Xs)) → VARMAT_IN_GA(Xs)

The TRS R consists of the following rules:

varmat_in_ga([]) → varmat_out_ga([])
varmat_in_ga(.(L, Ls)) → U3_ga(Ls, varmat_in_ga(L))
varmat_in_ga(.(black, Xs)) → U5_ga(varmat_in_ga(Xs))
varmat_in_ga(.(white, Xs)) → U6_ga(varmat_in_ga(Xs))
U3_ga(Ls, varmat_out_ga(VL)) → U4_ga(VL, varmat_in_ga(Ls))
U5_ga(varmat_out_ga(VXs)) → varmat_out_ga(.(black, VXs))
U6_ga(varmat_out_ga(VXs)) → varmat_out_ga(.(w, VXs))
U4_ga(VL, varmat_out_ga(VLs)) → varmat_out_ga(.(VL, VLs))

The set Q consists of the following terms:

varmat_in_ga(x0)
U3_ga(x0, x1)
U5_ga(x0)
U6_ga(x0)
U4_ga(x0, x1)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: